(declare-const v0 Bool)
(declare-const v1 Bool)
(push)
(assert v1)
(declare-const v20 Bool)
(check-sat)
(assert (xor v0 (= v1 v0 v1 (and v0 v0 v1 v1 v1 v0 v1 v1) (and v0 v0 v1 v1 v1 v0 v1 v1) v0 v0 v1 (and v0 v0 v1 v1 v1 v0 v1 v1) v0) (= v1 v0 v1 (and v0 v0 v1 v1 v1 v0 v1 v1) (and v0 v0 v1 v1 v1 v0 v1 v1) v0 v0 v1 (and v0 v0 v1 v1 v1 v0 v1 v1) v0) (= v1 v0 v1 (and v0 v0 v1 v1 v1 v0 v1 v1) (and v0 v0 v1 v1 v1 v0 v1 v1) v0 v0 v1 (and v0 v0 v1 v1 v1 v0 v1 v1) v0) (bvule (concat #x98 #x98) (concat #x98 #x98)) v1))
(declare-const _5-0 (_ BitVec 5))
(assert (=> (distinct (_ bv0 5) _5-0) (xor v0 true v20)))
(check-sat)
